\begin{tabbing}
R{-}state{-}var($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;${\it tr}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\oplus$$k$$\in$${\it ks}$.@$i$ effect $k$(v:Valtype(${\it da}$;$k$))  $x$ := $\lambda$$s$,$v$. ${\it tr}$($k$,$s$,$v$,$s$($x$)) State(${\it ds}$ $\oplus$ $x$ : $T$) v \+
\\[0ex]$\oplus$ @$i$ only events in ${\it ks}$ change $x$:$T$
\-
\end{tabbing}